/**
 * Software Analysis and Verification 
 * @project: Verify Pattern Matching with Guards in Scala
 * @authors: Mirco Dotta and Philippe Suter
 */


package ch.epfl.lara.patterns.ast;

/** 
 * AST for formulas
 */
sealed abstract class Formula


case class Imply (left: Formula, right: Formula) extends Formula {
   override def toString = "(" + left + " --> " + right + ")"
 }

case class Or (left: Formula, right: Formula) extends Formula {
  override def toString = "(" + left + " | " + right + ")"
}

case class And (left: Formula, right: Formula) extends Formula {
  override def toString = "(" + left + " & " + right + ")"
}

case class Not (formula: Formula) extends Formula {
  override def toString = "~(" + formula + ")"
}

case class Forall(name: Element, formula: Formula) extends Formula {
  override def toString = "(ALL " + name + "." + formula + ")"   
}

case class Exists(name: Element, formula: Formula) extends Formula {
  override def toString = "(EX " + name + "." + formula +")"  
}

abstract class Atom extends Formula

case class In (name: Element, set: Set) extends Atom {
  override def toString = name + " : " + set 
}

/** s1 subseteq s2 */
case class SubsetEq (s1: Set, s2: Set) extends Atom {
  override def toString = s1 + " \\subseteq " + s2
}

/** t1 = t2 */
case class Equal(e1: Term, e2: Term) extends Atom {
  override def toString = e1 + " = " + e2 
}

/** t1 < t2 */
case class Less(e1: Element, e2: Element) extends Atom {
  override def toString = e1 + " < " + e2
}

/** t1 < t2 */
case class LessEq(e1: Element, e2: Element) extends Atom {
  override def toString = e1 + " <= " + e2
}

/** true */
case object True extends Atom {
  override def toString = "true"
}

/** false */
case object False extends Atom {
  override def toString = "false"
}


abstract class Term {
  def getName: String = this match {
    case VarSet(name) => name
    case Var(name) => name
  }
}

abstract class Set extends Term

case class VarSet (name: String) extends Set {
  override def toString = name + ""
}

case class Singleton (e: Element) extends Set {
  override def toString = "{ " + e + " }"
}

abstract class Element extends Term

case class Var(name: String) extends Element {
  override def toString = name + ""
}

case class TypedVar(name: String, typez: String) extends Element {
  override def toString = "("+name + " :: " + typez +")"
}


/** function calls with one parameter.. used as representation for fields. */
case class FunctionCall(name: Var, param: Element) extends Element {
  override def toString = name + "(" + param + ")"
}

abstract class PrimitiveValue extends Element

case class IntValue(value: Int) extends PrimitiveValue {
 override def toString  = value + ""
}
